\begin{tabbing}
aframe{-}p(${\it es}$;$i$;$k$;$L$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$alle{-}at(${\it es}$;$i$;$e$.\=es{-}kind(${\it es}$; $e$) $=$ $k$ $\in$ Knd\+
\\[0ex]$\Rightarrow$ (\=$\forall$$x$:Id.\+
\\[0ex](\=$\neg$es{-}after(${\it es}$; $x$; $e$) $=$ es{-}when(${\it es}$; $x$; $e$) $\in$ es{-}vartype(${\it es}$; $i$; $x$)\+
\\[0ex]$\Rightarrow$ ($x$ $\in$ $L$ $\in$ Id))
\-\\[0ex]\& (\=$\neg$($x$ $\in$ $L$ $\in$ Id)\+
\\[0ex]$\Rightarrow$ \=es{-}after(${\it es}$; $x$; $e$)\+
\\[0ex]$=$
\\[0ex]es{-}when(${\it es}$; $x$; $e$)
\\[0ex]$\in$ es{-}vartype(${\it es}$; $i$; $x$))))
\-\-\-\-
\end{tabbing}